$\forall$$T$:Type, $P$:(($T$ List)$\rightarrow$Prop).
\\[0ex]($\forall$$L$:$T$ List. Dec($P$($L$))) $\Rightarrow$ ($\forall$$L$:$T$ List. Dec($\exists$${\it L'}$:$T$ List. ${\it L'}$ $\leq$ $L$ \& $P$(${\it L'}$)))